Natural Encoding of the Inner Space

ОМ ЛЯМБДА ГАРБХА ХУМ

Нетипизированное лямбда исчисление открыто было как часть языка пространства
для виратульных машин, минималистичный внутренний язык выражается достаточно
хорошо в LISP синтаксисе, где присутсвуют зачатки индуктивных конструкций, как
нумералы Черча и cons конструктор который ставился в основу сущности языка в
виде коренного слога. Основные конструкции этого языка являются по своей сути
набором конструкторов неких индуктивных типов: cons, nil, eq, atom, car, cdr,
lambda, curry, apply и id.

     O := I | λ I → O | O O

Первая попытка привести все в порядок — создание типизированной версии лямбда
исчисления, языка ML, основывалась на категорные модели в минимальной степени,
и все чаще этот пробел в нахождении оптимального выражение языка пространства
через категорные методы восполнялся категорными языками типа Charity или CPL.

     O := ∅ | ( O ) |
          □ | ∀ ( I : O ) → O |
          * | λ ( I : O ) → O |
          I | O → O | O O

Ближе всего к чистому языку пространства приблизился Lean прувер, так как
внутри него нет ничего кроме чистого CoC исчисления, предикативных универсумов
и синтаксических макро расширений. Другие языки имеют дополнительное число
аксиом, увеличивая ядро, а вместе с ним и путь, необходимый для организации
метациркуляции. Мы хотим построить язык, где кодирование индуктивных типов
базируется на категориальной семантике компиляции в CoC, все остальные
синтаксические конструкции являются индуктивными расширениями AST. AST базового
языка CoC тоже описывается индуктивными конструкциями и таким образом доступно
в макросах. В сущости язык полиномиальных функторов (data и record) и язык-ядро
исчисления процессов (spawn, receive и send) — это макросистема над CoC, ее
синтаксические расширения.

В чистом CoC у нас есть только стрелки, поэтому все способы кодирования
индуктивных типов — это вариации кодировки Черча. Самая расширенная кодировка
на момент публикации — это кодировка Church-Boehm-Berrarducci, которая
позволяет кодировать (ко)индуктивные типы. Другие известные кодировки это
кодировка Scott и Parigot.

     I := #identifier

     O := ∅ | ( O ) |
          □ | ∀ ( I : O ) → O |
          * | λ ( I : O ) → O |
          I | O → O | O O

     L := ∅ | L I

     A := ∅ | A ( L : O ) | A O

     F := ∅ | F ( I : O ) | ()

     P := I O , P | I O

     E := ∅ | E data L : A := F
            | E record L : A [ extend P ] := F
            | E let F in O
            | E case O [ | I O -> O ]
            | E receive O [ | I O -> O ]
            | E spawn O raise L := O
            | E send O to O

Была построена математическая модель кодировки, которая вычисляет (ко)лимиты в
заданых категориях, т.е. вычисляет в категорной модели инициальный объекты,
индуктивные типы. Будем называть такую кодировку в честь леммы Ламбека, которая
и гарантируем нам тождество (ко)инициального объекта в категории (ко)алгебр,
состоящих из конструкторов этого индуктивного типа. Такая кодировка оптимальнее
кодировки Беррардуччи, работает с зависимыми типами, а ее консистетность
гарантируется доказательством категорной формулировки этого утверждения в
системе Lean.

ОМ А ХУМ